A, B:Realizer.
R-Feasible(A)
 R-Feasible(B)
 (i:Id
 (((j:Id. R-has-loc(A;j) = i = j  )
 (& kdom(R-da(A;i)). 

 (& T=R-da(A;i)(k)  
 (& T(isrcv(k))
 (&  (((source(lnk(k)) = i  Id)  (T r R-da(B;destination(lnk(k)))(k)?Top))
 (&  & ((destination(lnk(k)) = i  Id)  (R-da(B;source(lnk(k)))(k)?Void r T)))))
 R-icompat(B;A) 

latex

Definitions	{T}, SQType(T), True, T, , P  Q, P  Q, x. t(x), t  T, xdom(f). v=f(x)   P(x;v), P & Q, x:A. B(x), P  Q, x:A. B(x), x(s)
Lemmas	R-interface-iff, Id sq, assert-eq-id, true wf, squash wf, R-interface-iff2, es realizer wf, R-Feasible wf, ldst wf, fpf-cap wf, fpf-ap wf, lnk wf, lsrc wf, isrcv wf, top wf, fpf wf, fpf-trivial-subtype-top, R-da wf, Kind-deq wf, fpf-dom wf, assert wf, Knd wf, eq id wf, R-has-loc wf, bool wf, Id wf, R-interface-icompat